\section{Setup Script}\label{sec:script}
\lstinputlisting[language=bash,mathescape=false]{setup_hol4.sh}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "lassie-tutorial"
%%% End:
